$\forall$$T_{1}$, $T_{2}$:Type, $r_{1}$:($T_{1}$$\rightarrow$$T_{1}$$\rightarrow\mathbb{P}$), $r_{2}$:($T_{2}$$\rightarrow$$T_{2}$$\rightarrow\mathbb{P}$).
\\[0ex]($T_{1}$ = $T_{2}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T_{1}$. \{$r_{1}$($x$,$y$) $\Leftarrow\!$ $r_{2}$($x$,$y$)\})
\\[0ex]$\Rightarrow$ \{WellFnd\{i\}($T_{1}$;$x$,$y$.$r_{1}$($x$,$y$)) $\Rightarrow$ WellFnd\{i\}($T_{2}$;$x$,$y$.$r_{2}$($x$,$y$))\}